COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub[let,jmc]" source
C00004 00003	#. %2eqshape[x,y]%1 is true if the S-expressions x and y have the
C00005 00004	#. Prove that %2eqshape%1 is an equivalence relation, i.e. prove
C00006 00005	#. %2shapes n%1 is a list of the distinct shapes that have n atoms. Each
C00007 00006	#. Write a logical formula that expresses the correctness of the
C00008 00007	#. A queue may be represented by cons cell whose qa-part points to
C00009 00008	.skip to column 1
C00010 00009	#. Sketch a proof that %2∀x. l-rotate r-rotate x = x%1.  For any
C00011 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "→"
CS206∂(30)FINAL EXAMINATION→FALL 1984
.turn off "→"

	This examination is open book and notes.
Write LISP functions or predicates and make proofs
 as follows except where something else is
requested.  Either notation may be used.
Be sure to indicate in an emphatic way the logical sentences indicating
what is to be proved and the %AF%*'s of any inductions that need to be
made.  You may assume that your functions are total but will be
suitably penalized if they aren't.

#. %2eqshape[x,y]%1 is true if the S-expressions ⊗x and ⊗y have the
same shape, i.e. the same car-cdr chains reach atoms in the two
expressions.  5 points

#. Prove that %2eqshape%1 is an equivalence relation, i.e. prove
%2∀x.eqshape(x,x)%1 and %2∀x y.eqshape(x,y) ⊃ eqshape(y,x)%1 and
%2∀x y z.eqshape(x,y) ∧ eqshape(y,z) ⊃ eqshape(x,z)%1.
15 points.

#. %2shapes n%1 is a list of the distinct shapes that have ⊗n atoms. Each
shape is represented by a single S-expression of that shape each of whose
atoms is A.  Thus 

%2shapes%1 4 = ((A.(A.(A.A))) (A.((A.A).A)) ((A.A).(A.A)) ((A.(A.A)).A) (((A.A).A).A))).

I have left out the spaces that Common Lisp would want and produce in
the example.  Don't worry about it. 15 points.

#. Write a logical formula that expresses the correctness of the
function %2shapes%1.  Don't try to prove it. 15 points.

#. A queue may be represented by ⊗cons cell whose qa-part points to
a list of the members of the queue and whose qd-part points to the last
word of the list.  Such a queue is shown in the figure.  The dirty
Lisp function  %2insert[x,q]%1 returns a queue that has had ⊗x inserted
as the last element of the queue ⊗q.  The dirty Lisp function
%2remove q%1 returns a list whose sole element is the first element
of the queue ⊗q and as a side effect removes the element from the
queue.  If the queue is empty, %2remove q =%1 NIL.  20 points.
.skip 10
.skip to column 1
#. %2l-rotate x%1 is the result of rotating the S-expression ⊗x to the
left preserving the shape.  Thus %2l-rotate%1_(A_._(B_._C))_=_(B_._(C_._A)).
Similarly %2r-rotate x%1 is the result of rotating ⊗x to the right.
The program should be in pure Lisp, i.e. shouldn't modify the existing
structure.

Hint: l-rotate and r-rotate are analogous to the lcyle and rcycle that
operate on lists.  However, using this analogy requires rather fancy
analogues of qa, qd and ⊗cons.  This problem may be fairly difficult.
15 points.

#. Sketch a proof that %2∀x. l-rotate r-rotate x = x%1.  For any
propositions to be proved by induction, show the induction statement.
15 points.